Nuprl Lemma : qabs_wf
11,40
postcript
pdf
r
:rationals. qabs(
r
)
rationals
latex
Definitions
qabs(
r
)
,
t
T
,
x
:
A
.
B
(
x
)
,
subtype(
S
;
T
)
Lemmas
int
inc
rationals
,
qmul
wf
,
rationals
wf
,
qpositive
wf
,
ifthenelse
wf
origin
r:rationals. qabs(r) 
rationals r:rationals. qabs(r) rationals Tx:A. B(x)